(set-logic NIA)
(set-option :model_validate true)
(set-option :model true)
(set-option :smt.arith.solver 6)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(push 1)
(push 1)
(pop 1)
(pop 1)
(push 1)
(assert (forall ((q0 Int) (q1 Int) (q2 Bool)) v2))
(pop 1)
(push 1)
(declare-const v16 Bool)
(declare-const i3 Int)
(declare-const v17 Bool)
(declare-const i4 Int)
(push 1)
(pop 1)
(declare-const i5 Int)
(pop 1)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(push 1)
(declare-const v23 Bool)
(push 1)
(declare-const v24 Bool)
(push 1)
(declare-const v25 Bool)
(assert (or v21 (distinct i1 (mod 82 i1)) (> 36 82) v9))
(assert (or v21 v25))
(assert (or (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82))))
(assert (or (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v20 v21 (<= (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82) i2)))
(assert (or (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3) (distinct i1 (mod 82 i1)) (< (* 321 (* (- (mod 82 i1)) 82) (- (* (- (mod 82 i1)) 82) (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1)) 82) (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3)))
(assert (or (< (* 321 (* (- (mod 82 i1)) 82) (- (* (- (mod 82 i1)) 82) (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1)) 82)))
(assert (or v22))
(assert (or v20 v14))
(assert (or (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3) v25 v9 v20 (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v2 (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v7 v5))
(assert (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v2))
(assert (or v25))
(assert (or v9 v20 (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3)))
(assert (or v22 (=> v10 v2) v9 (> 36 82)))
(assert (or v22 v25))
(assert (or v22 v2 (< (* 321 (* (- (mod 82 i1)) 82) (- (* (- (mod 82 i1)) 82) (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1)) 82) v21 v9 (> 36 82) (<= (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82) i2) v5))
(assert (or v21 v7))
(assert (or (distinct i1 (mod 82 i1)) (= v1 (= v14 v6 (=> v3 v3) v11 (=> v3 v3) v10 v12 v7 v11 v1) (>= 36 (- (mod 82 i1))) v14 (>= 36 (- (mod 82 i1))) v4 v14) v14 v5 v14 v14 v25))
(assert (or (distinct i1 (mod 82 i1)) (<= (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82) i2) (> 36 82) v23))
(assert (or v9 v23))
(assert (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9))))
(assert (or v22))
(assert (or (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v20 (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3) (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3) v22))
(assert (or v21 v25 v23 v23 v25 (<= (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82) i2) v14 v25))
(assert (or (distinct (* (- (mod 82 i1)) 82) (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82)) (distinct i1 (mod 82 i1)) v7))
(assert (or v22))
(assert (or v23 v22))
(assert (or v5))
(assert (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v21 v25 (= v1 (= v14 v6 (=> v3 v3) v11 (=> v3 v3) v10 v12 v7 v11 v1) (>= 36 (- (mod 82 i1))) v14 (>= 36 (- (mod 82 i1))) v4 v14) (=> v10 v2) v9 v25 v20))
(assert (or v2))
(assert (or v22 (= v1 (= v14 v6 (=> v3 v3) v11 (=> v3 v3) v10 v12 v7 v11 v1) (>= 36 (- (mod 82 i1))) v14 (>= 36 (- (mod 82 i1))) v4 v14)))
(assert (or v20))
(assert (or v21))
(assert (or (distinct (* (- (mod 82 i1)) 82) (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82)) (> 36 82) v7))
(assert (or (=> v10 v2) v22))
(assert (or v7 v20))
(assert (or v14))
(assert (or (> 36 82) v22 v22))
(assert (or (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82))))
(assert (or v2))
(assert (or v23 v22 v23))
(assert (or (<= (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82) i2)))
(assert (or (distinct i1 (mod 82 i1)) v7))
(assert (or (=> v10 v2)))
(assert (or v9 (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v9 v9 (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v7 v7 (< (* 321 (* (- (mod 82 i1)) 82) (- (* (- (mod 82 i1)) 82) (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1)) 82) (< (* 321 (* (- (mod 82 i1)) 82) (- (* (- (mod 82 i1)) 82) (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1)) 82) v23 (distinct (* (- (mod 82 i1)) 82) (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82))))
(assert (or (distinct (* (- (mod 82 i1)) 82) (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82))))
(assert (or v9))
(assert (or v23))
(assert (or (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3)))
(assert (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v22 v5 v22 v20 (> 36 82) (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) (= v1 (= v14 v6 (=> v3 v3) v11 (=> v3 v3) v10 v12 v7 v11 v1) (>= 36 (- (mod 82 i1))) v14 (>= 36 (- (mod 82 i1))) v4 v14) v14 v7))
(assert (or v20 (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3)))
(assert (or (distinct i1 (mod 82 i1))))
(assert (or (=> v10 v2)))
(assert (or v25 v23 v22 v23))
(assert (or v20 v23 v25))
(assert (or v2 (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3)))
(assert (or v14 v23 (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v14 (< (* 321 (* (- (mod 82 i1)) 82) (- (* (- (mod 82 i1)) 82) (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1)) 82) v2 (<= (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82) i2) v25 v14 (distinct (* (- (mod 82 i1)) 82) (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82)) v7 v25 (distinct (* (- (mod 82 i1)) 82) (+ (- (- (mod 82 i1)) i2 i2 (mod 82 i1) (mod 82 i1)) i1 565 82 82))))
(assert (or (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82))))
(assert (or v5 (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v25 (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v25 (=> v10 v2) (or (=> (> 36 82) (xor (distinct (- (mod 82 i1)) (* (- (mod 82 i1)) 82)) v3 v9 v15 v9)) v3)))
(check-sat)
(exit)
